Skip to content

feat(Geometry/Euclidean/Angle): add the Alternate segment theorem#41121

Open
Scarlett-le wants to merge 2 commits into
leanprover-community:masterfrom
Scarlett-le:tangent-chord-angle
Open

feat(Geometry/Euclidean/Angle): add the Alternate segment theorem#41121
Scarlett-le wants to merge 2 commits into
leanprover-community:masterfrom
Scarlett-le:tangent-chord-angle

Conversation

@Scarlett-le

@Scarlett-le Scarlett-le commented Jun 28, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Adds the Alternate segment theorem toMathlib/Geometry/Euclidean/Angle/Sphere.lean:
if a line is tangent to a sphere s at p₁
and p₁, p₂, p₃ lie on s, then twice the oriented angle from the tangent to the chord
p₁p₂ equals twice the inscribed angle subtending p₁p₂ at p₃. As elsewhere in this file,
the angles are doubled because the underlying oriented angles agree only mod π.

Dependencies

@github-actions

github-actions Bot commented Jun 28, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 5d8e57a95d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff (regex)

+ IsTangentAt.two_zsmul_oangle_eq_pi
+ two_zsmul_oangle_tangent_eq

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 5d8e57a).

  • +2 new declarations
  • −0 removed declarations
+EuclideanGeometry.Sphere.IsTangentAt.two_zsmul_oangle_eq_pi
+EuclideanGeometry.Sphere.two_zsmul_oangle_tangent_eq

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 5d8e57a95d
Reference commit 88d006abbc

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions Bot added the t-euclidean-geometry Affine and axiomatic geometry label Jun 28, 2026
felixpernegger
felixpernegger reviewed Jun 28, 2026
View reviewed changes
Comment thread Mathlib/Geometry/Euclidean/Angle/Sphere.lean Outdated
Comment thread Mathlib/Geometry/Euclidean/Angle/Sphere.lean Outdated
felixpernegger
felixpernegger reviewed Jun 28, 2026
View reviewed changes

@felixpernegger felixpernegger left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

awaiting-author

@Scarlett-le Scarlett-le mentioned this pull request Jun 29, 2026
Closed
@mathlib-dependent-issues mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 30, 2026
mathlib-bors Bot pushed a commit that referenced this pull request Jul 1, 2026
@Scarlett-le @j-loreaux
feat(Geometry/Euclidean/Sphere): add lemmas about points on a sphere (#…
ad6b660 
…41143)

Adds three lemmas to `Mathlib/Geometry/Euclidean/Sphere/Basic.lean`.

- `Sphere.ne_center_of_mem_of_mem_of_ne`: a point of a sphere that differs
  from another point of the sphere is not its center. Extracted at a
  reviewer's suggestion; this fact was reproved inline four times across
  #41121 and #41123.

- `norm_vsub_center_eq_radius`: for a point `p` on a sphere `s`,
  `‖p -ᵥ s.center‖ = s.radius`. This pattern occurs ten times in #34164 and
  four more times in the present file (twice in `inner_vsub_center_vsub_pos`
  and twice in `Sphere.dist_center_lt_radius_of_sbtw`); those four in-file
  occurrences are golfed to use it here.

- `Sphere.center_mem_affineSpan_pair_iff_isDiameter`: for two distinct points
  of a sphere, the center lies on the line through them if and only if those
  points are the endpoints of a diameter.

No mathematical content changes; the existing proofs are only shortened.

Co-authored-by: Scarlett-le <735979178@qq.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
@mathlib-dependent-issues mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 1, 2026
@mathlib-dependent-issues

mathlib-dependent-issues Bot commented Jul 1, 2026

Copy link
Copy Markdown

This PR/issue depends on:

@mathlib-merge-conflicts

mathlib-merge-conflicts Bot commented Jul 1, 2026

Copy link
Copy Markdown

This pull request has conflicts, please merge master and resolve them.

@mathlib-merge-conflicts mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 1, 2026
@Scarlett-le
Scarlett-le force-pushed the tangent-chord-angle branch from 4c35f5c to 5d8e57a Compare July 2, 2026 03:01
@github-actions github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 2, 2026
joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Jul 4, 2026
@Scarlett-le @j-loreaux @joelriou
feat(Geometry/Euclidean/Sphere): add lemmas about points on a sphere (l…
22e7d0a 
…eanprover-community#41143)

Adds three lemmas to `Mathlib/Geometry/Euclidean/Sphere/Basic.lean`.

- `Sphere.ne_center_of_mem_of_mem_of_ne`: a point of a sphere that differs
  from another point of the sphere is not its center. Extracted at a
  reviewer's suggestion; this fact was reproved inline four times across
  leanprover-community#41121 and leanprover-community#41123.

- `norm_vsub_center_eq_radius`: for a point `p` on a sphere `s`,
  `‖p -ᵥ s.center‖ = s.radius`. This pattern occurs ten times in leanprover-community#34164 and
  four more times in the present file (twice in `inner_vsub_center_vsub_pos`
  and twice in `Sphere.dist_center_lt_radius_of_sbtw`); those four in-file
  occurrences are golfed to use it here.

- `Sphere.center_mem_affineSpan_pair_iff_isDiameter`: for two distinct points
  of a sphere, the center lies on the line through them if and only if those
  points are the endpoints of a diameter.

No mathematical content changes; the existing proofs are only shortened.

Co-authored-by: Scarlett-le <735979178@qq.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
michaellee94 pushed a commit to michaellee94/mathlib4 that referenced this pull request Jul 11, 2026
@Scarlett-le @j-loreaux @michaellee94
feat(Geometry/Euclidean/Sphere): add lemmas about points on a sphere (l…
b44daec 
…eanprover-community#41143)

Adds three lemmas to `Mathlib/Geometry/Euclidean/Sphere/Basic.lean`.

- `Sphere.ne_center_of_mem_of_mem_of_ne`: a point of a sphere that differs
  from another point of the sphere is not its center. Extracted at a
  reviewer's suggestion; this fact was reproved inline four times across
  leanprover-community#41121 and leanprover-community#41123.

- `norm_vsub_center_eq_radius`: for a point `p` on a sphere `s`,
  `‖p -ᵥ s.center‖ = s.radius`. This pattern occurs ten times in leanprover-community#34164 and
  four more times in the present file (twice in `inner_vsub_center_vsub_pos`
  and twice in `Sphere.dist_center_lt_radius_of_sbtw`); those four in-file
  occurrences are golfed to use it here.

- `Sphere.center_mem_affineSpan_pair_iff_isDiameter`: for two distinct points
  of a sphere, the center lies on the line through them if and only if those
  points are the endpoints of a diameter.

No mathematical content changes; the existing proofs are only shortened.

Co-authored-by: Scarlett-le <735979178@qq.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
@jsm28

jsm28 commented Jul 20, 2026

Copy link
Copy Markdown
Contributor

maintainer merge

@github-actions

github-actions Bot commented Jul 20, 2026

Copy link
Copy Markdown

🚀 Pull request has been placed on the maintainer queue by jsm28.

@mathlib-triage mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 20, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer
@felixpernegger felixpernegger felixpernegger left review comments
Reviewers whose approvals may not affect merge requirements

Assignees

@jsm28 jsm28

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-euclidean-geometry Affine and axiomatic geometry

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@Scarlett-le @jsm28 @felixpernegger